$\forall$${\it es}$:ES, ${\it Sys}$:AbsInterface(Top), ${\it chain}$:(E(${\it Sys}$)$\rightarrow$(Id List)), $x$, $y$:Id.
\\[0ex]cr{-}fails{-}before(${\it es}$; ${\it Sys}$; ${\it chain}$; $x$; $y$) $\in$ $\mathbb{P}$